\begin{tabbing}
es{-}p{-}le{-}pred(${\it es}$;$P$)($e$,${\it e'}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=es{-}le(${\it es}$;${\it e'}$;$e$)\+
\\[0ex]\& $P$(${\it e'}$)
\\[0ex]\& ($\forall$${\it e''}$:es{-}E(${\it es}$). es{-}le(${\it es}$;${\it e''}$;$e$) $\Rightarrow$ es{-}locl(${\it es}$; ${\it e'}$; ${\it e''}$) $\Rightarrow$ ($\neg$($P$(${\it e''}$))))
\-
\end{tabbing}